\begin{tabbing}
$\forall$${\it da}$:fpf(Knd; $k$.Type), $k$:Knd.
\\[0ex]normal{-}da\=\{i:l\}\+
\\[0ex](${\it da}$)
\-\\[0ex]$\Rightarrow$ ($\uparrow$fpf{-}dom(Kind{-}deq; $k$; ${\it da}$))
\\[0ex]$\Rightarrow$ normal{-}type\=\{i:l\}\+
\\[0ex](fpf{-}cap(${\it da}$; Kind{-}deq; $k$; void))
\-
\end{tabbing}